T:Type, a:T List, x:T. l_disjoint(T;a;[x])  (x  a) 

latex

Definitions	t  T, x:A. B(x), (x  l), A, P & Q, P  Q, False, Prop, P  Q, P  Q, x. t(x), l_disjoint(T;l1;l2)
Lemmas	iff functionality wrt iff, all functionality wrt iff, not functionality wrt iff, and functionality wrt iff, member singleton, iff wf, not wf, l member wf